\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $a$:ecl(${\it ds}$; ${\it da}$), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]($\forall$$L$:(event{-}info(${\it ds}$;${\it da}$) List). 
\\[0ex](ecl{-}trans{-}normal($v$)
\\[0ex]$\wedge$ ($\forall$$n$:$\mathbb{N}^{+}$. (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($n$,$L$)) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($v$))))
\\[0ex]$\wedge$ \=($\forall$$n$:$\mathbb{N}$. \+
\\[0ex]($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\wedge$ (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)($n$,${\it L'}$))))
\-\\[0ex]$\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($n$,$L$)))
\-\\[0ex]$\wedge$ ($\forall$$m$:$\mathbb{N}$. (ecl{-}act(${\it ds}$; ${\it da}$; $m$; $a$)($L$)) $\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $v$)($m$,$L$))))
\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$. \+
\\[0ex]($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\wedge$ (0 $<$ $n$)
\\[0ex]$\wedge$ (\=star{-}append(event{-}info(${\it ds}$;${\it da}$); (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)(0)); (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)($n$)))\+
\\[0ex](${\it L'}$))))
\-\-\\[0ex]$\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; reset{-}ecl{-}tuple($v$))($n$,$L$)))
\-
\end{tabbing}